$\forall$$T$:Type, $P$:($T$$\rightarrow$Prop). ($\exists$!$x$:$T$. $P$($x$)) $\in$ Prop